Inference at * 1 3 1 1 
Iof proof for Lemma last-not-before:



1. T : Type
2. L : T List
3. (null(L))
4. no_repeats(T;L)
5. x : T
6. last(L) before x  L
7. x, y:T. x before y  L  ((x = y))
8. (last(L) = x)
9. x before last(L)  L
10. last(L) before last(L)  L
11. (last(L) = last(L))
  False 

latex

 by ((D (-1)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

A, P  Q, False